$\forall$$M$:MsgA, $k$:Knd, $s$:$M$.state, $v$:$M$.da($k$). $\neg$ma{-}has{-}effect($M$;$k$) $\Rightarrow$ ($\lambda$$x$.$M$.ef($k$,$x$,$s$,$v$)?$s$($x$)) $=$ $s$